rtag(${\it info}$; $e$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case ${\it info}$($e$) of inl($p$) =$>$ $\cdot$ $\mid$ inr($q$) =$>$ $q$.2